\begin{tabbing}
$\vdash$  \=$\forall$$T_{1}$,$T_{2}$:Type, $r_{1}$:($T_{1}$$\rightarrow$$T_{1}$$\rightarrow\mathbb{P}$), $r_{2}$:($T_{2}$$\rightarrow$$T_{2}$$\rightarrow\mathbb{P}$).\+
\\[0ex]($T_{1}$ = $T_{2}$)
\\[0ex]$\Rightarrow$ ($\forall$$x$,$y$:$T_{1}$. \{$r_{1}$($x$,$y$) $\Leftarrow\!$ $r_{2}$($x$,$y$)\})
\\[0ex]$\Rightarrow$ \{WellFnd\{i\}($T_{1}$;$x$,$y$.$r_{1}$($x$,$y$)) $\Rightarrow$ WellFnd\{i\}($T_{2}$;$x$,$y$.$r_{2}$($x$,$y$))\}
\-
\end{tabbing}